• Merge the modules ALoc, LVar and Var into the Id module that handles string IDs.
  • Defined an id as type +'a t = string, which is opaque to outside modules.
  • Defines the polymorphic variants lvar, var, loc and aloc.
  • Defines the aliases any_var = [ var | lvar ], any_loc = [ loc | aloc ], substable = [ lvar | var | aloc ], and any = [ lvar | var | loc | aloc ].
  • Define the modules ALoc, LVar, Var and Loc that contain allocation methods, and from/to string functions. Currently the from/to string conversion doesn't do any checking.
• Replace all instances of string LVars with Id.lvar Id.t: Expr.LVar,Exists,ForAll SLCmd.Fold,Unfold, Cmd.Call (for bindings), Pred.pred_definitions, Lemma.lemma_existentials,Spec.ss_label.
• Use the new Id type in Gil_syntax:
  • Relevant changes are in GillianCore/GIL_Syntax/Gil_syntax.mli
  • Replace all instances of string Vars with Id.var Id.t: Expr.PVar, LCmd.FreshSVar, Cmd.Assignement,LAction,Call,ECall,Apply,Arguments,PhiAssignement, Pred.pred_params, Lemma.lemma_params, Macro.macro_params, Spec.spec_params, BiSpec.bi_spec_params, Proc.proc_params
  • Replace all instances of mixed LVars and Vars with Id.any_var Id.t: SLCmd.ApplyLem,SepAssert,Invariant,Consume.
• Whenever possible, replaced uses of SS (string set) with a typed set (e.g. ALoc.Set).
• Updated WISL, C, C2, JS and transformers to match these types. For JS in particular, I tried making it work with the least amount of changes, so there might be odd places where we jump between raw strings and typed IDs quite a bit; otherwise I would've had to rework too much code.

Resolves #7